q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
↳ QTRS
↳ DependencyPairsProof
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
Q3(y(x1)) → Y(q3(x1))
Y(q1(b(x1))) → Q2(y(y(x1)))
Q3(y(x1)) → Q3(x1)
A(q2(y(x1))) → A(y(x1))
Q0(a(x1)) → Q1(x1)
Q1(y(x1)) → Q1(x1)
Q0(y(x1)) → Q3(x1)
Q0(y(x1)) → Y(q3(x1))
A(q1(b(x1))) → A(y(x1))
A(q1(b(x1))) → Q2(a(y(x1)))
A(q2(y(x1))) → Q2(a(y(x1)))
Y(q2(y(x1))) → Q2(y(y(x1)))
Y(q2(a(x1))) → Y(a(x1))
Q1(a(x1)) → A(q1(x1))
A(q2(a(x1))) → Q2(a(a(x1)))
Y(q1(b(x1))) → Y(x1)
Y(q2(a(x1))) → Q2(y(a(x1)))
Y(q2(y(x1))) → Y(y(x1))
Y(q1(b(x1))) → Y(y(x1))
Q1(y(x1)) → Y(q1(x1))
A(q2(a(x1))) → A(a(x1))
A(q1(b(x1))) → Y(x1)
Q2(x(x1)) → Q0(x1)
Q1(a(x1)) → Q1(x1)
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
Q3(y(x1)) → Y(q3(x1))
Y(q1(b(x1))) → Q2(y(y(x1)))
Q3(y(x1)) → Q3(x1)
A(q2(y(x1))) → A(y(x1))
Q0(a(x1)) → Q1(x1)
Q1(y(x1)) → Q1(x1)
Q0(y(x1)) → Q3(x1)
Q0(y(x1)) → Y(q3(x1))
A(q1(b(x1))) → A(y(x1))
A(q1(b(x1))) → Q2(a(y(x1)))
A(q2(y(x1))) → Q2(a(y(x1)))
Y(q2(y(x1))) → Q2(y(y(x1)))
Y(q2(a(x1))) → Y(a(x1))
Q1(a(x1)) → A(q1(x1))
A(q2(a(x1))) → Q2(a(a(x1)))
Y(q1(b(x1))) → Y(x1)
Y(q2(a(x1))) → Q2(y(a(x1)))
Y(q2(y(x1))) → Y(y(x1))
Y(q1(b(x1))) → Y(y(x1))
Q1(y(x1)) → Y(q1(x1))
A(q2(a(x1))) → A(a(x1))
A(q1(b(x1))) → Y(x1)
Q2(x(x1)) → Q0(x1)
Q1(a(x1)) → Q1(x1)
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
Y(q1(b(x1))) → Q2(y(y(x1)))
A(q2(y(x1))) → A(y(x1))
A(q1(b(x1))) → A(y(x1))
A(q1(b(x1))) → Q2(a(y(x1)))
A(q2(y(x1))) → Q2(a(y(x1)))
Y(q2(y(x1))) → Q2(y(y(x1)))
Y(q2(a(x1))) → Y(a(x1))
Q1(a(x1)) → A(q1(x1))
A(q2(a(x1))) → Q2(a(a(x1)))
Y(q1(b(x1))) → Y(x1)
Y(q2(a(x1))) → Q2(y(a(x1)))
Y(q2(y(x1))) → Y(y(x1))
Y(q1(b(x1))) → Y(y(x1))
A(q2(a(x1))) → A(a(x1))
A(q1(b(x1))) → Y(x1)
Used ordering: Polynomial interpretation [25,35]:
Q3(y(x1)) → Y(q3(x1))
Q3(y(x1)) → Q3(x1)
Q0(a(x1)) → Q1(x1)
Q1(y(x1)) → Q1(x1)
Q0(y(x1)) → Q3(x1)
Q0(y(x1)) → Y(q3(x1))
Q1(y(x1)) → Y(q1(x1))
Q2(x(x1)) → Q0(x1)
Q1(a(x1)) → Q1(x1)
The value of delta used in the strict ordering is 5/16.
POL(Q1(x1)) = 1/2 + (4)x_1
POL(y(x1)) = (4)x_1
POL(x(x1)) = (4)x_1
POL(q0(x1)) = (2)x_1
POL(bl(x1)) = 0
POL(q2(x1)) = 1/4 + (2)x_1
POL(b(x1)) = 4 + (4)x_1
POL(Q2(x1)) = 1/2 + (1/4)x_1
POL(Q0(x1)) = 1/2 + x_1
POL(q3(x1)) = 0
POL(q1(x1)) = (2)x_1
POL(Q3(x1)) = 1/2
POL(a(x1)) = (4)x_1
POL(Y(x1)) = 1/2 + (5/4)x_1
POL(q4(x1)) = 4 + (9/4)x_1
POL(A(x1)) = (4)x_1
q0(a(x1)) → x(q1(x1))
q1(y(x1)) → y(q1(x1))
q1(a(x1)) → a(q1(x1))
a(q2(a(x1))) → q2(a(a(x1)))
a(q1(b(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
Q3(y(x1)) → Y(q3(x1))
Q3(y(x1)) → Q3(x1)
Q0(a(x1)) → Q1(x1)
Q1(y(x1)) → Y(q1(x1))
Q1(y(x1)) → Q1(x1)
Q0(y(x1)) → Q3(x1)
Q1(a(x1)) → Q1(x1)
Q2(x(x1)) → Q0(x1)
Q0(y(x1)) → Y(q3(x1))
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
Q1(y(x1)) → Q1(x1)
Q1(a(x1)) → Q1(x1)
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
Q1(y(x1)) → Q1(x1)
Q1(a(x1)) → Q1(x1)
The value of delta used in the strict ordering is 16.
POL(Q1(x1)) = (4)x_1
POL(y(x1)) = 4 + (4)x_1
POL(a(x1)) = 4 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
Q3(y(x1)) → Q3(x1)
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
Q3(y(x1)) → Q3(x1)
The value of delta used in the strict ordering is 4.
POL(y(x1)) = 1 + (4)x_1
POL(Q3(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))